\begin{tabbing}
$\forall$\=${\it es}$:ES, $C$, $T$:Type, $R_{1}$, $R_{2}$:($C$$\rightarrow$E$\rightarrow\mathbb{P}$), ${\it decodes}_{1}$:($i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $R_{1}$($i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$),\+
\\[0ex]${\it decodes}_{2}$:($i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $R_{2}$($i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$), ${\it dec\_R}_{1}$:($i$:$C$$\rightarrow$$e$:E$\rightarrow$Dec($R_{1}$($i$,$e$))).
\-\\[0ex]($\forall$$i$:$C$, $e$:E. $\neg$($R_{1}$($i$,$e$) \& $R_{2}$($i$,$e$)))
\\[0ex]$\Rightarrow$ \=($\forall$$i$:$C$, $e$:\{$x$:E$\mid$ ($R_{1}$($i$,$x$)) $\vee$ ($R_{2}$($i$,$x$))\} , ${\it st}$:state@loc($e$).\+
\\[0ex](($R_{1}$($i$,$e$)) $\Rightarrow$ ([$R_{1}$ ? ${\it decodes}_{1}$ : ${\it decodes}_{2}$]($i$,$e$,${\it st}$) = ${\it decodes}_{1}$($i$,$e$,${\it st}$)))
\\[0ex]\& (($R_{2}$($i$,$e$)) $\Rightarrow$ ([$R_{1}$ ? ${\it decodes}_{1}$ : ${\it decodes}_{2}$]($i$,$e$,${\it st}$) = ${\it decodes}_{2}$($i$,$e$,${\it st}$))))
\-
\end{tabbing}